ds:fpf(Id; x.Type), es:event_system{i:l}, e:es-E(es).
@loc(e) discrete ds
 (t:rationals. es-state-after-elapsed(es; e; t) = es-state-after(es; e)  decl-state(ds)) 

latex

Definitions

t  T, x:A. B(x), loc(e), P  Q, es-state(es; i), decl-state(ds), es-state-after(es; e), ma-state(ds), x:AB(x), top, id-deq, Id, Type, x.A(x), x. t(x), fpf-cap(f; eq; x; z), es-state-after-elapsed(es; e; t), atom{$n:n}, x:A  B(x), fpf(A; a.B(a)), event_system{i:l}, t.1, es-E(es), fpf-all(A; eq; f; x,v.P(x;v)), @i discrete ds, quotient(A; x,y.B(x;y)), rationals, f(a), <a, b>, s = t, fpf-ap(f; eq; x), es-dtype(es; i; x; T), void, isect(A; x.B(x)), b, A, b, , prop{i:l}, if b then t else f fi , fpf-dom(eq; x; f), P  Q, P  Q, Unit, left + right, es-vartype(es; i; x), let x,y = A in B(x;y), case b of inl(x) => s(x) | inr(y) => t(y)

Lemmas

eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, fpf-trivial-subtype-top, bool wf, bnot wf, not wf, assert wf, equal-top, discrete-after-elapsed, fpf-ap wf, rationals wf, es-dds wf, es-E wf, event system wf, fpf wf, es-state-after-elapsed wf, fpf-cap wf, Id wf, id-deq wf, top wf, es-state-after wf, es-state-subtype2, es-loc wf